poss:(ES{i}{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss){i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}), Rs:(TT{i'}).
Trans(T;_1,_2.Rs(_1,_2))
 (es:ES{i}, e:E.
 (poss(es))
  (discrete state@i r T)
  (loc(e) = i)
  (Rs((discrete state when e),(discrete state after e))))
 (es:ES{i}.
 (poss(es))
  (discrete state@i r T)
  @i stable s.ma-knows{i:l}
  @i stable s.ma-knows(poss; i; T; s; P; Rs; R)  ) 

latex

Definitions

{T}, P  Q, x:A. B(x), SQType(T), t  T, s ~ t, Id, s = t, Atom$n, discrete state@i, , (discrete state when e), x:A  B(x), b, ES, f(a), t.1, E, PossibleEvent(poss), pe-es(e), pe-state(p), x:AB(x), Type, Trans(T;x,y.E(x;y)), A c B, P & Q, poss-consistent(i;T;s;ev;R), x,y. t(x;y), EqDecider(T), Unit, left + right, IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), Top, let x,y = A in B(x;y), pred!(e;e'), SWellFounded(R(x;y)), Void, x:A.B(x), S  T, suptype(S; T), first(e), A, loc(e), <a, b>, x. t(x), kind(e), loc(e), pe-loc(p), a = b, P  Q, P  Q, e@i. P(e), x.A(x), K(P)@e, @i stable state.P(state)  , Ki(P)@s, (discrete state after e), , pe-e(p)

Lemmas

pe-e wf, all functionality wrt iff, implies functionality wrt iff, eq id wf, assert-eq-id, pe-loc wf, pe-es wf, poss-consistent wf, es-E wf, subtype rel wf, es-loc wf, es-dstate wf, deq wf, EOrderAxioms wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, trans wf, possible-event wf, Id wf, event system wf, pe-state wf, es-dstate-when wf, es-dstate-after wf, Id sq